T:Type, L1, L2:(T List). rev(L1)  rev(L2)  L1  L2 

latex

Definitions	s ~ t, <a, b>, A c B, , P  Q, left + right, {T}, A List, , as @ bs, [car / cdr], False, (x  l), P & Q, P  Q, increasing(f;k), x:A. B(x), x:A  B(x), True, [], P  Q, rev(as), x:A. B(x), P  Q, L1  L2, type List, x:AB(x), s = t, t  T, Type
Lemmas	iff wf, sublist wf, reverse wf, nil sublist, false wf, append wf, rev implies wf, cons sublist nil, implies functionality wrt iff, cons sublist cons, sublist append, sublist append1, sublist transitivity, reverse-reverse